4.4. 归纳类型🔗

归纳类型 是在 Lean 中引入新类型的主要方式。虽然宇宙、函数以及商类型是内置的原语类型，用户无法自行添加，但 Lean 里的其它类型要么是归纳类型，要么是基于宇宙、函数与归纳类型定义的。归纳类型的定义依赖于它们的 类型构造子 和 构造子 ；它们的其它性质也由这些定义推导而来。每个归纳类型有唯一的类型构造子，这个构造子可能带有宇宙参数和普通参数。归纳类型可以拥有任意数量的构造子；这些构造子用于生成新的值，其类型由归纳类型的类型构造子决定。

根据归纳类型的类型构造子和构造子，Lean 会自动生成一个 递归子。从逻辑上讲，递归子代表归纳原则或消去规则；从计算角度看，它们表示原始递归计算。递归函数的终止性由其翻译为递归子的调用来保证，因此 Lean 的内核只需对递归子的应用做类型检查，而无需单独进行终止性分析。除此之外，Lean 还根据递归子生成很多辅助结构无论类型是否递归，递归子总会被用到，这些结构被系统的其他部分使用。

结构体 是一种特殊的归纳类型，只包含一个构造子。当一个结构体被声明时，Lean 会自动生成辅助工具，使得新结构体能支持更多语言特性。

本节描述用于定义归纳类型和结构体的具体语法细节、归纳类型声明会在环境中引入哪些新的常量和定义，以及在编译后归纳类型值的运行时表现。

4.4.1. 归纳类型声明🔗

语法归纳类型声明

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructors.
For example, `List α` is the list of elements of type `α`, and is defined as follows:
```
inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)
```
A list of elements of type `α` is either the empty list, `nil`,
or an element `head : α` followed by a list `tail : List α`.
See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
for more information.
inductive `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。optDeclSig where
        (| `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers ident `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。optDeclSig)*
      (deriving ident,*)?

声明一个新的归纳类型。 declModifiers 的含义可在声明修饰词部分查询。

声明归纳类型后，其类型构造子、构造子和递归子会添加到环境中。新的归纳类型扩展了 Lean 的核心逻辑——它们不是由系统中已有的数据编码或模拟出来的。归纳类型声明还必须满足一系列良构性要求以确保逻辑系统的一致性。

声明的第一行，从 Lean.Parser.Command.inductive : commandinductive 到 Lean.Parser.Command.inductive : commandwhere，指定新类型构造子的名称和类型。如果为类型构造子提供了类型签名，则其结果类型必须是宇宙，但参数不一定是类型。如果没有提供签名，Lean 会尝试推断出恰好足以容纳结果类型的宇宙。在某些情况下，这一过程可能无法找到最小宇宙，甚至完全无法找到合适的宇宙，此时必须给出标注。

构造子定义在 Lean.Parser.Command.inductive : commandwhere后边。构造子并非必需，比如像 False 和 Empty 这样没有构造子的归纳类型是完全合理的。每个构造子定义以竖线 ('|', Unicode 'VERTICAL BAR' (U+007c))、声明修饰词和名字。名字是原始标识符。名字后接声明签名。签名可以包含任意参数，但需满足归纳类型声明的良构性要求，返回类型必须是归纳类型的类型构造子的饱和应用。如果未指定签名，则 Lean 会插入足够的隐式参数来推断出良构的返回类型。

新归纳类型的名字定义在当前命名空间中。每个构造子的名字位于该归纳类型的命名空间下。

4.4.1.1. 参数与索引🔗

类型构造子可以接收两类参数：参数和索引。定义中，参数必须在整个归纳类型定义中保持一致；所有构造子中出现的类型构造子，参数必须一模一样。索引则可以在不同构造子的类型构造子的具体应用中变化。所有参数在类型构造子的签名中必须排在索引的前面。

在类型构造子的签名中冒号（':'）之前的内容作为整个归纳类型声明的参数，这些参数在类型定义过程中始终如一。通常，冒号之后为索引，可以在归纳类型定义中变化。但如果 inductive.autoPromoteIndices 选项为 true，则本来可以作为参数的语法层面的索引会被自动提升为参数。当一个索引的所有类型依赖全都是参数类型，且它在所有构造子的类型构造子调用中始终未实例化、未变化，那么它就可以被当作参数。

选项

inductive.autoPromoteIndices

默认值：true

只要有可能，就应将归纳类型中的索引提升为参数。

索引实际上定义了一个类型族。每次索引取值确定，就从族中选出一个类型，该类型有它各自的构造子。含索引的类型构造子即定义了一个 索引族 。

4.4.1.2. 归纳类型样例🔗

一个没有构造子的类型

Vacant 是一个空的归纳类型，等价于 Lean 的 Empty 类型：

inductive Vacant : Type where

空归纳类型并非毫无用处；它们可以用于标记不可达代码。

在线查看 ↪

一个没有构造子的命题

No 是一个假命题，等价于 Lean 的 False:

inductive No : Prop where

在线查看 ↪

单位类型

Solo 和 Lean 的 Unit 类型等价：

inductive Solo where
  | solo

这是一个类型构造子和构造子的签名都被省略的例子。Lean 会将 Solo 推断为 Type：

Solo : Type#check Solo

Solo : Type

构造子的名字是 Solo.solo，因为构造子的名字位于类型构造子的命名空间下。由于 Solo 无需参数，Lean 自动推断 Solo.solo 的签名为：

Solo.solo : Solo#check Solo.solo

Solo.solo : Solo

在线查看 ↪

真命题

Yes 等价于 Lean 的 True 命题：

inductive Yes : Prop where
  | intro

不同于 One，新的归纳类型 Yes 被指定为 Prop 宇宙。

Yes : Prop#check Yes

Yes : Prop

推断得到的 Yes.intro 的签名如下：

Yes.intro : Yes#check Yes.intro

Yes.intro : Yes

在线查看 ↪

一个带参数和索引的类型

EvenOddList α b 表示一种列表，其中 α 是元素类型，b 为 true 表示含偶数个元素：

inductive EvenOddList (α : Type u) : Bool → Type u where
  | nil : EvenOddList α true
  | cons : α → EvenOddList α isEven → EvenOddList α (not isEven)

以下例子类型合法，因为列表有两个元素：

example : EvenOddList String true :=
  .cons "a" (.cons "b" .nil)

以下例子类型不合法，因为列表有三个元素：

example : EvenOddList String true :=
  Type mismatch
  EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil))
has type
  EvenOddList String !!!true
but is expected to have type
  EvenOddList String true.cons "a" (.cons "b" (.cons "c" .nil))

Type mismatch
  EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil))
has type
  EvenOddList String !!!true
but is expected to have type
  EvenOddList String true

在本声明中，α 是参数，因为它在 EvenOddList 的每次出现都保持一致；b 是索引，因为它在不同出现中可取不同值。

在线查看 ↪

参数在冒号前和冒号后

在本例中，所有参数都在 Either 签名的冒号前：

inductive Either (α : Type u) (β : Type v) : Type (max u v) where
  | left : α → Either α β
  | right : β → Either α β

在下面这个版本中，有两个名为 α 的类型，它们可能并不相同：

inductive Either' (α : Type u) (β : Type v) : Type (max u v) where
  Mismatched inductive type parameter in
  Either' α β
The provided argument
  α
is not definitionally equal to the expected parameter
  α✝

Note: The value of parameter `α✝` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.| left : {α : Type u} → {β : Type v} → α → Either' α β
  | right : β → Either' α β

Mismatched inductive type parameter in
  Either' α β
The provided argument
  α
is not definitionally equal to the expected parameter
  α✝

Note: The value of parameter `α✝` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.

把参数放在冒号后，则对应的构造子参数可以由构造子自行实例化：

inductive Either'' : Type u → Type v → Type (max u v + 1) where
  | left : {α : Type u} → {β : Type v} → α → Either'' α β
  | right : β → Either'' α β

此时需要更大的宇宙层级，因为构造子的参数必须处于比归纳类型本身更低的宇宙。 Either''.right 的类型参数会按 Lean 的自动隐式参数规则推断。

在线查看 ↪

4.4.1.3. 匿名构造子语法🔗

如果归纳类型只有一个构造子，则这个构造子可以使用 匿名构造子语法。即，不必写出构造子的名字并将其应用到参数上，而直接把所有显式参数用尖括号（'⟨' 和 '⟩', Unicode MATHEMATICAL LEFT ANGLE BRACKET (U+0x27e8) 和 MATHEMATICAL RIGHT ANGLE BRACKET (U+0x27e9)）括起来，并用逗号分隔即可。这种语法可以用于模式匹配和表达式。若想按照参数名字提供参数，或将所有隐式参数变为显式，则需使用普通构造子语法。

语法匿名构造子

可通过用尖括号括起所有显式参数并用逗号分隔，匿名地调用构造子。

term ::= ...
    | 如果期望类型是只有一个构造器 `c` 的归纳类型，那么*匿名构造器* `⟨e, ...⟩` 等价于 `c e ...`。
如果给出的项比 `c` 的参数更多，其余参数会组成新的匿名构造器应用。
例如，`⟨a, b, c⟩ : α × (β × γ)` 等价于 `⟨a, ⟨b, c⟩⟩`。⟨ term,* ⟩

匿名构造子

类型 AtLeastOne α 和 List α 相似，区别在于它始终至少有一个元素：

inductive AtLeastOne (α : Type u) : Type u where
  | mk : α → Option (AtLeastOne α) → AtLeastOne α

可采用匿名构造子语法进行构造：

def oneTwoThree : AtLeastOne Nat :=
  ⟨1, some ⟨2, some ⟨3, none⟩⟩⟩

也可用该语法进行模式匹配：

def AtLeastOne.head : AtLeastOne α → α
  | ⟨x, _⟩ => x

同样，传统构造子语法也可以：

def oneTwoThree' : AtLeastOne Nat :=
  .mk 1 (some (.mk 2 (some (.mk 3 none))))

def AtLeastOne.head' : AtLeastOne α → α
  | .mk x _ => x

在线查看 ↪

4.4.1.4. 派生实例🔗

归纳类型声明末尾可选的 Lean.Parser.Command.inductive : commandderiving 子句，可用于自动派生类型类实例。详情请见关于实例自动派生的章节。

4.4.2. 结构体声明🔗

语法结构体声明

command ::= ...
    | `declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers
      structure `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId `optDeclSig` 匹配类型可选的声明签名：先是一列绑定器，随后可以有 `: type`。bracketedBinder* (: term)?
        (extends (ident : )?term,*)?
        where
        (`declModifiers` 是声明修饰符的集合，包括：

* 文档注释 `/-- ... -/`
* 属性列表 `@[attr1, attr2]`
* 可见性说明符 `private` 或 `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` 或 `nonrec`

所有修饰符都是可选的，并且必须按上述顺序出现。
`nestedDeclModifiers` 与 `declModifiers` 相同，但属性与声明打印在同一行；它用于嵌套在其他语法中的声明，例如结构体字段。declModifiers ident ::)?
        structFields
      (deriving derivingClass,*)?

声明一个新的结构体类型。

结构体 是只有一个构造子、无下标的归纳类型。作为这些约束的交换，Lean 会为结构体自动生成一些便捷功能：为每个字段生成投影函数、允许基于字段名（而非位置参数）的新构造语法、同样可以按指定字段名修改值，并且结构体可以扩展其它结构体。结构体和其它归纳类型一样，可以递归定义；它们必须遵守严格正性限制。结构体本身并没有带来 Lean 表达力的增强；它们的所有特性都是通过代码生成机制实现的。

4.4.2.1. 结构体参数🔗

与普通归纳类型声明相同，结构体声明的头部可以包含参数和结果宇宙层级。结构体不能定义索引族。

4.4.2.2. 字段🔗

结构体声明的每个字段都对应构造子的一个参数。

Inferring Universes

The structure MyProd is the same as Prod.

structure MyProd (α β : Type _) where
  fst : α
  snd : β

The two parameters and the two fields are constructor parameters:

MyProd.mk.{u, v}
  {α : Type u}
  {β : Type v}
  (fst : α)
  (snd : β)
  : MyProd.{u, v} α β

Additionally, the constructor is universe polymorphic; the type constructor MyProd takes two universe parameters:

MyProd.{u, v} (α : Type u) (β : Type v) : Type (max u v)

The universe level of each type of each field must be less than or equal to the universe level of the structure. Lean infers that Type (max u v) is the least universe that can accommodate both Type u and Type v.

在线查看 ↪

每个字段都会独立插入自动隐式参数，即使它们的名称相同；这些字段随后成为对类型进行量化的构造子参数。

Auto-Implicit Parameters in Structure Fields

The structure MyStructure contains fields whose types have auto-implicit parameters:

structure MyStructure where
  field1 : Fin n
  field2 : Fin n

Each fields in the constructor MyStructure.mk takes its own implicit parameter n of type Nat:

MyStructure.mk
  (field1 : {n : Nat} → Fin n)
  (field2 : {n : Nat} → Fin n)
  : MyStructure

The type constructor MyStructure takes no universe parameters, and the resulting type is in Type, which is the universe for Nat and Fin n:

MyStructure : Type

在线查看 ↪

对于每个字段，都会自动生成一个 投影函数，用于从构造子中提取字段的值。这个函数在结构体名称对应的命名空间中。结构体字段投影由精译器特别处理（具体见结构体继承），其行为比仅查找命名空间要复杂。当字段类型依赖于之前字段时，依赖型投影函数的类型会使用之前的投影表达，而不是显式模式匹配。

依赖型投影类型

结构体 ArraySized 包含一个字段，其类型依赖于结构体参数和先前字段：

structure ArraySized (α : Type u) (length : Nat)  where
  array : Array α
  size_eq_length : array.size = length

投影函数 size_eq_length 的签名中，会隐式带入结构体类型的参数，通过先前的投影引用之前的字段：

ArraySized.size_eq_length.{u}
  {α : Type u} {length : Nat}
  (self : ArraySized α length)
  : self.array.size = length

在线查看 ↪

结构体字段可以通过 := 指定默认值。如果没有提供该字段的显式值，则使用默认值。

默认值

图的邻接表可用一个 Nat 列表的数组表示。数组大小代表顶点数，数组中每个元素（通过顶点下标访问）存储对应顶点的出边。由于 adjacency 字段提供了默认值 #[]，空图 Graph.empty 在构造时无需提供字段值。

structure Graph where
  adjacency : Array (List Nat) := #[]

def Graph.empty : Graph := {}

在线查看 ↪

结构体字段还可以通过索引以点号访问。字段编号从 1 开始。

4.4.2.3. 结构体构造子🔗

结构体构造子可以通过在字段前加构造子名称与 :: 显式命名。若未显式指定名称，则构造子在结构体命名空间中名为 mk。声明修饰符也可被用于显式构造子名称前。

非默认构造子名称

结构体 Palindrome 包含一个字符串以及显示该字符串反转与原字相等的证明：

structure Palindrome where
  ofString ::
  text : String
  is_palindrome : text.`String.data` has been deprecated: Use `String.toList` insteaddata.reverse = text.`String.data` has been deprecated: Use `String.toList` insteaddata

其构造子为 Palindrome.ofString，而非 Palindrome.mk。

在线查看 ↪

结构体构造子的修饰符

结构体 NatStringBimap 维护自然数与字符串之间的有限双射。它由一对映射组成，每个映射的键在另一个映射的值中恰好出现一次。由于构造子是 private，定义模块之外的代码不能直接构造新实例，而必须使用维护类型不变式的 API。此外，显式给出默认构造子名称也提供了为构造子附加文档注释的机会。

structure NatStringBimap where
  /--
  在一些自然数和字符串之间构建一个有限双射
  -/
  private mk ::
  natToString : Std.HashMap Nat String
  stringToNat : Std.HashMap String Nat

def NatStringBimap.empty : NatStringBimap := ⟨{}, {}⟩

def NatStringBimap.insert
    (nat : Nat) (string : String)
    (map : NatStringBimap) :
    Option NatStringBimap :=
  if map.natToString.contains nat ||
      map.stringToNat.contains string then
    none
  else
    some <|
      NatStringBimap.mk
        (map.natToString.insert nat string)
        (map.stringToNat.insert string nat)

在线查看 ↪

由于结构体本质上就是单构造子的归纳类型，其构造子既可以直接调用或用于匿名构造子语法下的模式匹配, 也可以用 结构体实例 记法（含有实字段名和值）进行构造或模式匹配。

语法结构体实例

term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{ structInstField,*
        (: term)? }

指定字段名及其值来构造一个结构体类型的值。字段说明可有两种形式：

structInstField ::= ...
    | structInstLVal := private? term

structInstField ::= ...
    | ident

structInstLVal 可以是字段名（标识符）、字段索引（自然数），或带中括号的项，并可接零个或多个子字段。子字段可以是带点的字段名或索引，也可以是带中括号的项。

该语法在精译时会转换为结构体构造子的应用。字段以名称分配，顺序不限。子字段赋值用于初始化嵌套在字段中的结构体的字段。在构造结构体时不允许带中括号的项，中括号用于结构体更新。

不带 := 的字段被认为是字段缩写。此时，标识符 f 等价于 f := f，即作用域中的 f 会被用于字段赋值。

所有无默认值的字段，都需要明确提供。如果默认参数指定为 tactic，那么在精译阶段会运行 tactic 求得参数值。

在模式匹配语境下，字段名映射到能匹配相应投影的模式，字段缩写可直接绑定同名模式变量。默认参数同样适用于模式；如果模式未指定带默认值字段的值，则模式只匹配默认值。

When a field definition contains the Lean.Parser.Term.stuctInstFieldprivate modifier, the value is placed in the current module's private scope, even if the structure value is itself in the public scope. The value is wrapped in a public but non-exposed helper definition. This is particularly useful with instances of type classes, because the implementation of methods in public instances of type classes are exposed by default. This modifier allows them to be made private.

可选的类型标注允许在无法由上下文确定时显式指定结构体类型。

模式与默认值

结构体 AugmentedIntList 包含一个列表及一些额外信息；省略时额外信息为空：

structure AugmentedIntList where
  list : List Int
  augmentation : String := ""

在测试列表是否为空时，函数 isEmpty 还会检测字段 augmentation 是否为空；因为忽略字段会采用默认值，模式匹配同样如此：

def AugmentedIntList.isEmpty : AugmentedIntList → Bool
  | {list := [], augmentation := ""} => true
  | _ => false

false#eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty

false

在线查看 ↪

Private Field Values

Even when a definition of a structure is exposed, individual fields may be hidden using the field-level Lean.Parser.Term.stuctInstFieldprivate modifier. In this module, the exposed public definition of x may use the private definition secret because the imaginary field's value is not exposed:

Main.lean

module

public structure Complex where
  real : Float
  imaginary : Float

private def secret := 2.3

@[expose]
public def x : Complex := {
  real := 5.0
  imaginary := private 2 * secret
}

Private Methods

In this module, the existence of the State structure is public, but its constructor and field are private. The function State.toString is also private, and is intended to be accessed via the ToString instance. However, because the implementations of methods are exposed for public instances, this is not allowed:

Main.lean

module

public structure State where
  private mk ::
  private count : Nat

private def State.toString (s : State) : String :=
  s!"⟨{s.count}⟩"

public instance : ToString State where
  toString s := s.Invalid field `toString`: The environment does not contain `State.toString`, so it is not possible to project the field `toString` from an expression
  s
of type `State`

Note: A private declaration `State.toString` (from the current module) exists but would need to be public to access here.toString

Invalid field `toString`: The environment does not contain `State.toString`, so it is not possible to project the field `toString` from an expression
  s
of type `State`

Note: A private declaration `State.toString` (from the current module) exists but would need to be public to access here.

Marking the implementation of toString as private removes it from the module's public scope, giving it access to private functions:

Main.lean

module

public structure State where
  private mk ::
  private count : Nat

private def State.toString (s : State) : String :=
  s!"⟨{s.count}⟩"

public instance : ToString State where
  toString s := private s.toString

语法结构体更新

term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{term with
        structInstField,*
        (: term)?}

对构造子类型的值进行更新。 Lean.Parser.Term.structInst : termStructure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be inherited. If `e` is itself a variable called `x`, it can be elided: `fun y => { x := 1, y }`. A *structure update* of an existing value can be given via `with`: `{ point with x := 1 }`. The structure type can be specified if not inferable: `{ x := 1, y := 2 : Point }`.with 子句之前的项应为结构体类型值，即待更新的原值。新的结构体实例中，所有未指定的字段都从原始值拷贝，指定字段被覆盖为新值。更新结构体时，也可以通过中括号带索引更新数组字段。索引表达式不要求越界，越界更新会被忽略。

数组更新

结构体更新可以用字段名，也可以用数组索引。越界索引的更新会被直接忽略：

structure AugmentedIntArray where
  array : Array Int
  augmentation : String := ""
deriving Repr

def one : AugmentedIntArray := {array := #[1]}
def two : AugmentedIntArray := {one with array := #[1, 2]}
def two' : AugmentedIntArray := {two with array[0] := 2}
def two'' : AugmentedIntArray := {two with array[99] := 3}
({ array := #[1], augmentation := "" },
 { array := #[1, 2], augmentation := "" },
 { array := #[2, 2], augmentation := "" },
 { array := #[1, 2], augmentation := "" })#eval (one, two, two', two'')

({ array := #[1], augmentation := "" },
 { array := #[1, 2], augmentation := "" },
 { array := #[2, 2], augmentation := "" },
 { array := #[1, 2], augmentation := "" })

结构体类型的值也可以使用 Lean.Parser.Command.declValEqns : commandwhere，在定义后为每个字段赋值，只能用于定义体，不能在通用表达式中用。

结构体中的 where

Lean 中的乘积类型是名为 Prod 的结构体。可以用字段投影方式来给乘积类型赋值：

def location : Float × Float where
  fst := 22.807
  snd := -13.923

4.4.2.4. 结构体继承🔗

结构体可以通过可选的 Lean.Parser.Command.structure : commandextends 子句继承其它结构体。结果结构体类型将包含所有父结构体的全部字段。如果父结构体字段有重名，所有同名字段必须同类型。

继承结果结构体有一个 字段解析顺序，决定字段的最终取值。一般来说，该顺序采用 C3 线性化。即字段解析顺序是所有父结构体列表的一个全序排列（保留 extends 语句顺序），如果无法形成 C3 线性化，则采用启发式算法排序。结构体自身在解析顺序中最前。

字段解析顺序用于计算可选字段的默认值。如未指定字段值，则使用解析顺序中第一个定义了默认的值。默认值中若引用了其它字段，也采用字段解析顺序；这意味着子结构体如重写了父结构体的默认字段，也可影响父结构体的默认字段的计算结果。由于子结构体自带最高优先级，因此子结构体中的默认值优先生效于父结构体。

结构体继承其它结构体时，新结构体的构造子会接受父类型的信息作为附加参数。通常每个父结构体会作为一个参数传递，其值包含父结构体的全部字段。如果父结构体有重叠字段，则只保留不重叠的那部分，以避免字段重复。

父类型与子类型之间没有子类型关系。即使结构体 B 继承于 A，期望 A 的函数也不会接受 B 类型。但系统会自动生成转换函数，将结构体转为各自的父结构体类型。这些转换函数称为 父投影。父投影函数定义在子结构体的命名空间中，形式为父类型名加前缀 to。

结构体类型继承与字段重叠

In this example, a Textbook is a Book that is also an AcademicWork:

structure Book where
  title : String
  author : String

structure AcademicWork where
  author : String
  discipline : String

structure Textbook extends Book, AcademicWork

Textbook.toBook (self : Textbook) : Book#check Textbook.toBook

因为 author 字段同时出现在 Book 与 AcademicWork，所以 Textbook.mk 构造子只需传入一个父实例。其签名为：

Textbook.mk (toBook : Book) (discipline : String) : Textbook

转换函数为：

Textbook.toBook (self : Textbook) : BookTextbook.toAcademicWork (self : Textbook) : AcademicWork

后一函数会将包含的 Book 的 author 字段与独立的 Discipline 字段组合，等价于：

def toAcademicWork (self : Textbook) : AcademicWork :=
  let .mk book discipline := self
  let .mk _title author := book
  .mk author discipline

在线查看 ↪

最终结构体的投影用法上就像字段是所有父结构体字段的并集一样。 Lean 的精译器会在使用字段时自动生成合适的投影。同样，基于字段的初始化与结构体更新语法可以隐藏继承实现的细节。但如果直接使用构造子名称、匿名构造子语法，或者按索引而非字段名称引用字段时，这些细节是可见的。

字段索引与结构体继承

structure Pair (α : Type u) where
  fst : α
  snd : α
deriving Repr

structure Triple (α : Type u) extends Pair α where
  thd : α
deriving Repr

def coords : Triple Nat := {fst := 17, snd := 2, thd := 95}

对 coords 的第一个字段索引求值时，得到的是底层的 Pair，而不是字段 fst 的内容：

{ fst := 17, snd := 2 }#eval coords.1

{ fst := 17, snd := 2 }

精译器会自动将 coords.fst 转换为 coords.toPair.fst。

在线查看 ↪

无结构体子类型关系

如下定义偶数、偶质数和具体偶质数：

structure EvenNumber where
  val : Nat
  isEven : 2 ∣ val := by decide

structure EvenPrime extends EvenNumber where
  notOne : val ≠ 1 := by decide
  isPrime : ∀ n, n ≤ val → n ∣ val  → n = 1 ∨ n = val

def two : EvenPrime where
  val := 2
  isPrime := by⊢ ∀ (n : Nat), n ≤ 2 → n ∣ 2 → n = 1 ∨ n = 2
    introsn✝:Nata✝¹:n✝ ≤ 2a✝:n✝ ∣ 2⊢ n✝ = 1 ∨ n✝ = 2
    repeat' (cases ‹Nat.le _ _›step.step.refl.refla✝:0 ∣ 2⊢ 0 = 1 ∨ 0 = 2)
    all_goals omegaAll goals completed! 🐙

def printEven (num : EvenNumber) : IO Unit :=
  IO.print num.val

直接将 printEven 应用于 two 会产生类型错误：

printEven sorry : IO Unit#check printEven Application type mismatch: The argument
  two
has type
  EvenPrime
but is expected to have type
  EvenNumber
in the application
  printEven twotwo

Application type mismatch: The argument
  two
has type
  EvenPrime
but is expected to have type
  EvenNumber
in the application
  printEven two

因为 EvenPrime 类型的值并非 EvenNumber 类型值。

Lean.Parser.Command.print : command#print 命令能展示所有结构体类型的重要信息，包括父投影、所有字段（含默认值）、构造子及字段解析顺序。对于包含复杂继承菱形的层次结构而言，这些信息非常有用。

#print 与结构体类型

以下是关于自行车的结构体抽象，涵盖电动/非电动、大型/普通家庭自行车。最后一种结构体 ElectricFamilyBike 形成了继承图中的“菱形”，因为 FamilyBike 和 ElectricBike 都继承自 Bicycle。

structure Vehicle where
  wheels : Nat

structure Bicycle extends Vehicle where
  wheels := 2

structure ElectricVehicle extends Vehicle where
  batteries : Nat := 1

structure FamilyBike extends Bicycle where
  wheels := 3

structure ElectricBike extends Bicycle, ElectricVehicle

structure ElectricFamilyBike
    extends FamilyBike, ElectricBike where
  batteries := 2

Lean.Parser.Command.print : command#print 可以显示各结构体类型的重要信息：

structure ElectricBike : Type
number of parameters: 0
parents:
  ElectricBike.toBicycle : Bicycle
  ElectricBike.toElectricVehicle : ElectricVehicle
fields:
  Vehicle.wheels : Nat :=
    2
  ElectricVehicle.batteries : Nat :=
    1
constructor:
  ElectricBike.mk (toBicycle : Bicycle) (batteries : Nat) : ElectricBike
field notation resolution order:
  ElectricBike, Bicycle, ElectricVehicle, Vehicle#print ElectricBike

structure ElectricBike : Type
number of parameters: 0
parents:
  ElectricBike.toBicycle : Bicycle
  ElectricBike.toElectricVehicle : ElectricVehicle
fields:
  Vehicle.wheels : Nat :=
    2
  ElectricVehicle.batteries : Nat :=
    1
constructor:
  ElectricBike.mk (toBicycle : Bicycle) (batteries : Nat) : ElectricBike
field notation resolution order:
  ElectricBike, Bicycle, ElectricVehicle, Vehicle

默认情况下，ElectricFamilyBike 有三轮，因为在解析顺序中 FamilyBike 优先于

structure ElectricFamilyBike : Type
number of parameters: 0
parents:
  ElectricFamilyBike.toFamilyBike : FamilyBike
  ElectricFamilyBike.toElectricBike : ElectricBike
fields:
  Vehicle.wheels : Nat :=
    3
  ElectricVehicle.batteries : Nat :=
    2
constructor:
  ElectricFamilyBike.mk (toFamilyBike : FamilyBike) (batteries : Nat) : ElectricFamilyBike
field notation resolution order:
  ElectricFamilyBike, FamilyBike, ElectricBike, Bicycle, ElectricVehicle, Vehicle#print ElectricFamilyBike

structure ElectricFamilyBike : Type
number of parameters: 0
parents:
  ElectricFamilyBike.toFamilyBike : FamilyBike
  ElectricFamilyBike.toElectricBike : ElectricBike
fields:
  Vehicle.wheels : Nat :=
    3
  ElectricVehicle.batteries : Nat :=
    2
constructor:
  ElectricFamilyBike.mk (toFamilyBike : FamilyBike) (batteries : Nat) : ElectricFamilyBike
field notation resolution order:
  ElectricFamilyBike, FamilyBike, ElectricBike, Bicycle, ElectricVehicle, Vehicle

在线查看 ↪

4.4.3. 逻辑模型🔗

4.4.3.1. 递归子🔗

每一个归纳类型都拥有一个递归子。递归子的定义完全由类型构造子和数据构造子的类型签名所决定。递归子的类型是函数类型，但它们是原语级别的，不能用 fun 来定义。

4.4.3.1.1. 递归子类型🔗

递归子接收以下参数：

归纳类型的参数: 由于参数在整个定义中保持一致，因此递归子可以统一对这些参数进行抽象。
动机(motive): 动机决定了递归子的应用结果的类型。动机是一个函数，其参数是类型的指标及其具体实例。动机决定的类型所处的具体宇宙由归纳类型的宇宙层级和具体的数据构造子决定——详见子单元消去部分。
每个构造子的次要前提(minor premise): 对每个构造子，递归子都要求一个函数，证明动机对该构造子的任意应用成立。每个次要前提都会对该构造子的所有参数进行抽象。如果构造子的某个参数类型就是该归纳类型本身，那么次要前提还会接收一个额外参数，其类型是动机应用于该参数值的结果；它将接收递归处理这一递归参数所得的结果。
主要前提，或称目标: 最后，递归子接收一个该类型的实例作为参数，以及所有指标的值。

递归子的结果类型是将动机应用于这些指标和主要前提所得的类型。

Bool 的递归子

Bool 的递归子 Bool.rec 有如下参数：

动机给定一个 Bool 后，在任意宇宙中计算出一个类型。
两个构造子各有一个次要前提，分别说明动机对 false 和 true 成立。
主要前提是某个 Bool。

返回类型是动机应用于主要前提所得的类型。

Bool.rec.{u} {motive : Bool → Sort u}
  (false : motive false)
  (true : motive true)
  (t : Bool) : motive t

List 的递归子

List 的递归子 List.rec 有如下参数：

参数 α 位于最前，因为动机、次要前提和主要前提都需要引用它。
动机给定一个 List α 后，在任意宇宙中计算出一个类型；宇宙层级 u 与 v 彼此无关。
两个构造子各有一个次要前提：
- 动机对 List.nil 成立；
- 对 List.cons 的任意应用，只要动机对尾部成立，就应对整个列表成立。额外参数 motive tail 来自 tail 的类型中对 List 的递归出现。
主要前提是某个 List α。

同样，返回类型是动机应用于主要前提所得的类型。

List.rec.{u, v} {α : Type v} {motive : List α → Sort u}
  (nil : motive [])
  (cons : (head : α) → (tail : List α) → motive tail →
    motive (head :: tail))
  (t : List α) : motive t

带参数和指标的递归子

已知 EvenOddList 的定义如下：

inductive EvenOddList (α : Type u) : Bool → Type u where
  | nil : EvenOddList α true
  | cons : α → EvenOddList α isEven → EvenOddList α (not isEven)

递归子 EvenOddList.rec 与 List.rec 十分相似，差别来自指标：

动机会对任意选择的指标进行抽象。
nil 的次要前提把动机应用于该构造子的指标值 true。
cons 的次要前提对递归出现中使用的指标值进行抽象，并用其否定值实例化动机。
主要前提也会对任意选择的指标进行抽象。

EvenOddList.rec.{u, v} {α : Type v}
  {motive : (isEven : Bool) → EvenOddList α isEven → Sort u}
  (nil : motive true EvenOddList.nil)
  (cons : {isEven : Bool} →
    (head : α) →
    (tail : EvenOddList α isEven) → motive isEven tail →
    motive (!isEven) (EvenOddList.cons head tail)) :
  {isEven : Bool} → (t : EvenOddList α isEven) → motive isEven t

在线查看 ↪

当动机是一个返回 Prop 的谓词时，递归子就表现为归纳法。非递归构造子的分支是归纳的基本样例，而递归构造子所额外提供的参数就是归纳假设。

4.4.3.1.1.1. 子单元消去🔗

Lean 中的证明是计算无关的。换句话说，在给定了某个命题的证明之后，程序应该无法检测到到底是哪一个证明被接受了。这种思想体现在归纳定义的命题或谓词的递归子的类型中。对于这些类型，如果定理存在多种可能的证明方式，那么 motive 只能返回另一个 Prop。如果类型的结构保证了至多只存在一个证明，那么 motive 可以返回任意宇宙中的类型。拥有至多一个元素的命题被称为 子单元。 Lean 并不会强制用户去证明某命题只有唯一的证明，而是采用了一种保守的语法近似方法来检测一个命题是否为子单元。满足以下两个条件的命题会被视为子单元（subsingleton）：

至多只有一个构造子。
每个构造子的参数类型要么是 Prop，要么是参数或者索引。

True 是子单元

True 是子单元，因为它仅有一个无参数的构造子。它的递归子类型如下：

True.rec.{u} {motive : True → Sort u}
  (intro : motive True.intro)
  (t : True) : motive t

False 是子单元

False 是子单元，因为它没有构造子。它的递归子类型如下：

False.rec.{u} (motive : False → Sort u) (t : False) : motive t

注意动机是一个显式参数。因为它在后续参数类型中没有出现，因此不能自动推断它。

And 是子单元

And 是子单元，因为它仅有一个构造子，并且这个构造子的两个参数类型都是命题。它的递归子类型如下：

And.rec.{u} {a b : Prop} {motive : a ∧ b → Sort u}
  (intro : (left : a) → (right : b) → motive (And.intro left right))
  (t : a ∧ b) : motive t

Or 不是子单元

Or 不是子单元，因为它有多个构造子。它的递归子类型如下：

Or.rec {a b : Prop} {motive : a ∨ b → Prop}
  (inl : ∀ (h : a), motive (.inl h))
  (inr : ∀ (h : b), motive (.inr h))
  (t : a ∨ b) : motive t

动机的类型表明 Or.rec 只能用于产生证明。对析取命题提供的证明也能用来证明其它命题，但程序无法判别具体是哪个分支为真。

Eq 是子单元

Eq 是子单元，因为它只有一个构造子 Eq.refl。构造子会用参数值实例化 Eq 的索引，因此所有参数都是参数项：

Eq.refl.{u} {α : Sort u} (x : α) : Eq x x

它的递归子类型如下：

Eq.rec.{u, v} {α : Sort v} {x : α}
  {motive : (y : α) → x = y → Sort u}
  (refl : motive x (.refl x))
  {y : α} (t : x = y) : motive y t

意味着等式证明可以用来重写非命题类型的类型。

4.4.3.1.2. 规约🔗

归纳类型声明除了为逻辑添加新常量外，还会引入新的规约规则。这些规则负责处理递归子与构造子之间的互动，尤其是以构造子为主要前提的递归子应用。这种规约形式称为 ι-规约（iota reduction）。

当递归子的主要前提是没有递归参数的构造子时，递归子应用会规约为将该构造子的次要前提应用于构造子的参数。如果存在递归参数，则传给次要前提的对应参数由递归子应用于递归出现而得到。

4.4.3.2. 良构性约束🔗

归纳类型声明需要满足一系列良构性约束。这些约束确保当逻辑扩展进入新的归纳类型规则时，Lean 的逻辑系统依然保持一致。这些约束是保守的：一些不会破坏一致性的归纳类型会被这些约束拒绝。

4.4.3.2.1. 宇宙层级🔗

归纳类型的类型构造子必须处于某个宇宙中，或是返回类型为宇宙的函数类型。每个数据构造子的类型必须是返回饱和应用归纳类型的函数类型。如果归纳类型的宇宙是 Prop，则对宇宙没有进一步的限制，因为 Prop 是非直谓的。如果宇宙不是 Prop，那么以下要求必须成立，对每一个数据构造子的参数都适用：

若构造子的参数是归纳类型的参数（即参数 vs 索引），则该参数类型不能超过类型构造子的宇宙层级。
其它所有构造子参数的类型都必须严格小于类型构造子的宇宙层级。

宇宙、构造子和参数

Either 处于其两个参数宇宙层级的最大值，因为两个参数都是归纳类型的参数：

inductive Either (α : Type u) (β : Type v) : Type (max u v) where
  | inl : α → Either α β
  | inr : β → Either α β

CanRepr 的宇宙层级比构造子参数 α 要更高，因为 α 不是归纳类型的参数：

inductive CanRepr : Type (u + 1) where
  | mk : (α : Type u) → [Repr α] → CanRepr

无构造子的归纳类型的宇宙可以比参数的宇宙更小：

inductive Spurious (α : Type 5) : Type 0 where

但对 Spurious 若要添加构造子，其宇宙层级也必须做相应改变。

在线查看 ↪

4.4.3.2.2. 严格正性🔗

所有定义中的类型在构造子参数类型中的出现都必须处于严格正性的位置。如果一个类型不处于函数的参数类型里（无论嵌套了多少层函数类型），也不作为任何表达式（除归纳类型的类型构造子外）的参数，那它就是严格正性的位置。该限制用来排除不安全的归纳类型定义，虽有可能因此排除掉某些良构类型。

非严格正性的归纳类型

如果不拒绝类型 Bad，它会导致 Lean 不一致：

(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declaredinductive Bad where
  | bad : (Bad → Bad) → Bad

(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declared

之所以这样，是因为如果假定 Bad 成立，则可以构造出环状逻辑从而证明 False。 Bad.bad 会被拒绝，是因为构造子的参数类型是 Bad → Bad，也就是 Bad 作为函数参数出现。

下面这个不动点算子的声明会被拒绝，因为 Fix 作为参数出现在 f 中：

(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declaredinductive Fix (f : Type u → Type u) where
  | fix : f (Fix f) → Fix f

(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declared

Fix.fix 会被拒绝，因为 f 不是归纳类型的类型构造子，而 Fix 本身却作为它的参数出现。在这种情况下，Fix 也足以构造一个等价于 Bad 的类型：

def Bad : Type := Fix fun t => t → t

4.4.3.2.3. Prop vs Type🔗

Lean 会拒绝那些实际上无法多态使用的宇宙多态类型。例如，如果对宇宙参数的部分实例化会导致类型变成 Prop，而该类型又不是子单元，则其递归子只允许针对命题（即动机只能返回 Prop）。这些类型实际上只适合充当 Prop 本身，所以宇宙多态很可能本就是错误。由于这种类型几乎无实际意义，Lean 的归纳类型精译器并未设计为支持它们。

如果这种宇宙多态归纳类型本身是子单元，则这样的定义还是有意义的。 Lean 的标准库定义了 PUnit 和 PEmpty。若要定义既可属于 Prop 也可属于 Type 的子单元类型，可将选项 bootstrap.inductiveCheckResultingUniverse 设为 false。

选项

bootstrap.inductiveCheckResultingUniverse

默认值：true

默认情况下，如果归纳类型/结构体命令生成的宇宙不是零（universe level 0），即使对某些宇宙参数来说有可能是零，也会报告错误。原因：除非这个类型是子单元（subsingleton），否则这几乎不是用户想要的，因为它只能消去到 Prop（命题）。在 Init 前导库包中，我们定义了子单元，并通过此选项关闭该检查。在将来改进验证器之后，此选项可能会被删除。

过度使用宇宙多态的 Bool

不允许定义可处于任意宇宙中的 Bool 版本：

inductive PBool : Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
  Sort u

Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`Sort u where
  | true
  | false

Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
  Sort u

Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`

4.4.3.3. 用于终止性检查的构造🔗

These constructions follow the description in McBride, Goguen, and McKinna (2004)Conor McBride, Healfdene Goguen, and James McKinna, 2004. “A Few Constructions on Constructors”. In Types for Proofs and Programs, International Workshop, TYPES 2004. (LNCS 3839).

除了 Lean 核心类型理论为归纳类型规定的类型构造子、数据构造子和递归子外，Lean 还自动生成许多实用的辅助构造。首先，方程编译器（用于将带模式匹配的递归函数翻译为递归子应用）会用到这些额外构造：

recOn 是递归子的一个变体，其目标参数排在每个构造子的分支参数之前。
casesOn 也是一个变体，其目标参数也在分支之前，且递归参数不会产生归纳假设。它表达的是分情况分析而非原始递归。
below 生成一个类型，表达针对某动机，目标所有子树的所有归纳类型元素都满足该动机。它能把归纳/原始递归用的动机变成强递归/强归纳的动机。
brecOn 是使用 below 以可以访问所有子树（而不仅是直接递归参数）的递归子变体，表达强归纳。
noConfusion 是一个通用语句，可据此推出构造子的单射性和互斥性。
noConfusionType 是为 noConfusion 设计的动机，用以描述两个构造子相等时的推论。对不同构造子而言这是 False；相同构造子则为各自参数的等式。

对于良构递归，通常还需要一个通用意义上的“大小”概念。这正是 SizeOf 类型类所提供的。

类型类

SizeOf.{u} (α : Sort u) : Sort (max 1 u)
SizeOf.{u} (α : Sort u) : Sort (max 1 u)

SizeOf 是每一个归纳类型都会自动派生的类型类，它为该类型提供了一个到 Nat 的 “大小” 函数。默认实例会为每个构造子定义其 “大小” 等于 1 加上该构造子所有字段的“大小”之和。

这个机制通常用于良构（well-founded）证明，因为构造子的每个字段的“大小”都比整体构造子本身小，在许多情况下这就足以证明递归函数只会作用于更小的值。如果默认的证明策略失败，通常建议在函数定义时通过 termination_by 参数自定义一个大小度量。

实例构造子

SizeOf.mk.{u}

方法

sizeOf : α → Nat

一个元素的“大小”，是一个自然数，在每个归纳类型的字段上会递减。

4.4.4. 运行时表示🔗

归纳类型的运行时表示取决于构造子的数量、每个构造子参数的数量，以及参数是否相关。

4.4.4.1. 特例🔗

并非所有归纳类型都采用这里描述的表示——部分归纳类型由 Lean 编译器特别支持：

The representation of the fixed-width integer types UInt8, …, UInt64, Int8, …, Int64, and USize depends on whether the code is compiled for a 32- or 64-bit architecture. Their representation is described in a dedicated section.
Char 用 uint32_t 表示。由于 Char 取值不超过 21 位，所以总是无箱。
Float 由指向包含 double 的 Lean 对象的指针表示。
枚举归纳类型，即至少有 2 个、至多有 2^{32} 个构造子且每个构造子都无参数的类型，用 uint8_t、uint16_t、uint32_t 中足以为每个构造子分配唯一值的最小类型表示。例如，Bool 用 uint8_t 表示，false 为 0，true 为 1。
Decidable α 的表示与 Bool 相同。
Nat and Int are represented by lean_object *. Their representations are described in more detail in the section on natural numbers and the section on integers.

4.4.4.2. 相关性🔗

类型和证明在运行时没有表示形式。也就是说，若归纳类型处于 Prop，则其值会在编译前被抹除。同理，所有定理的陈述和类型都会被抹除。具有运行时表示的类型称为 相关类型，反之则为 无关类型。

类型是无关的

虽然 List.cons 的签名表面有三个参数：

List.cons.{u} {α : Type u} : α → List α → List α

但运行时实际上只有两个参数，因为类型参数是无关的，不参与运行时表示。

证明是无关的

虽然 Fin.mk 的签名表面有三个参数：

Fin.mk {n : Nat} (val : Nat) : val < n → Fin n

但运行时只有两个参数，因为证明会被抹除。

大多数情况下，无关的值在编译后直接消失。但在少数情况下（如它们是多态构造子的参数时），需要某种“形态”时，会以简单的值表示。

4.4.4.3. 平凡包装类型🔗

An inductive type is a trivial wrapper if it has has exactly one constructor and that constructor has exactly one run-time relevant parameter. Trivial wrappers are represented identically to their constructor's parameter in the following circumstances:

The inductive type is private.
The type is public, and the public scope of the module in which it is defined contains enough information to determine that it is a trivial wrapper.
The type is defined in a source file that is not a module.

如果归纳类型只有一个构造子，且该构造子只有一个运行时相关参数，则该归纳类型的运行时表示与其参数类型完全一致。

零负载子类型

结构体 Subtype 用于将某个类型的元素和满足某谓词的证明打包。其构造子需要四个参数，但其中三个参数是无关的：

Subtype.mk.{u} {α : Sort u} {p : α → Prop}
  (val : α) (property : p val) : Subtype p

因此，子类型在编译后不带来运行时额外开销，其表示和 val 字段的类型完全一致。

带符号整数

有符号整数类型 Int8、...、Int64、ISize 是只带唯一字段、该字段包装了对应无符号整数类型的结构体。因为结构体本身是平凡包装，它们分别表示为无符号 C 类型 uint8_t、...、uint64_t、size_t。

4.4.4.4. 其它归纳类型🔗

如果归纳类型不属于上述类别，则其运行时表示由其构造子结构决定。没有相关参数的构造子，仅以在构造子列表中的索引（无箱无符号机器整数）表示。有相关参数的构造子表示为一个对象，该对象有头部信息、构造子索引、指向其它对象的指针数组、以及按照类型分组排序的标量字段数组。头部用来追踪引用计数以及其它记账信息。

递归函数的编译生成过程与大多数编程语言一致，并不是利用归纳类型的递归子来实现。将递归函数翻译为递归子只是为了给出可靠的终止证据，而非用于实际执行代码。

4.4.4.4.1. FFI🔗

From the perspective of C, these other inductive types are represented by lean_object *. Each constructor is stored as a lean_ctor_object, and lean_is_ctor will return true.

There are no guarantees about the exact layout of fields in a constructor object; the compiler is free to select any layout. Thus, constructor objects should only be created or unpacked by functions defined in Lean code. These functions can be made available to C via the Lean.Parser.Attr.export : attrexport attribute. Because the resulting C and Lean code call symbols defined in each other, they should be linked together. Each C should be compiled to an object file using a custom target in Lake and added to the Lean library configuration's moreLinkObjs field.

4.4.5. 互递归归纳类型🔗

归纳类型之间可以互相递归。互递归的归纳类型需在 mutual ... end 代码块中统一声明。

互递归归纳类型

在前面的例子中，类型 EvenOddList 用 Boolean 索引来区分列表是偶数还是奇数长度。这个区分也可以用两个互递归类型 EvenList 和 OddList 表达：

mutual
  inductive EvenList (α : Type u) : Type u where
    | nil : EvenList α
    | cons : α → OddList α → EvenList α
  inductive OddList (α : Type u) : Type u where
    | cons : α → EvenList α → OddList α
end

example : EvenList String := .cons "x" (.cons "y" .nil)
example : OddList String := .cons "x" (.cons "y" (.cons "z" .nil))

example : OddList String := .cons "x" (.cons "y" Unknown constant `OddList.nil`

Note: Inferred this name from the expected resulting type of `.nil`:
  OddList String.nil)

Unknown constant `OddList.nil`

Note: Inferred this name from the expected resulting type of `.nil`:
  OddList String

在线查看 ↪

4.4.5.1. 要求🔗

mutual 块中的归纳类型视为一个整体；它们必须一起满足对非互递归归纳类型良构性条件的泛化要求。即便这些类型单独也可以用非互递归方式定义，只要它们放在 mutual 块内，也要集体满足这些要求。

4.4.5.1.1. 互相关系🔗

每个类型构造子的签名都必须能在不引用 mutual 组中其它归纳类型的情况下完成精译。换言之，mutual 组中的归纳类型不能互相作为参数。各归纳类型的构造子可以在参数类型中提及组内其它类型构造子，但必须满足由非互递归归纳类型的递归出现条件推广而来的限制。

类型构造子之间不能互相引用

Lean 不接受下述归纳类型：

mutual
  inductive FreshList (α : Type) (r : α → α → Prop) : Type where
    | nil : FreshList α r
    | cons (x : α) (xs : FreshList α r) (fresh : Fresh r x xs)
  Invalid mutually inductive types: Binder annotations for parameter `α` must matchinductive Fresh
      (r : α → Unknown identifier `FreshList`FreshList α → Prop) :
      α → Unknown identifier `FreshList`FreshList α r → Prop where
    | nil : Fresh r x .nil
    | cons : r x y → (f : Fresh r x ys) → Fresh r x (.cons y ys f)
end

类型构造子不能出现在同组另一个归纳类型的签名中，所以 FreshList 在 Fresh 的类型构造子中不可见：

Unknown identifier `FreshList`

4.4.5.1.2. 参数必须匹配🔗

同一个 mutual 组中的所有归纳类型，参数必须类型完全一致。索引可以不同。

Differing numbers of parameters

Even though Both and Optional are not mutually recursive, they are declared in the same mutual block and must therefore have identical parameters:

mutual
  inductive Both (α : Type u) (β : Type v) where
    | mk : α → β → Both α β
  Invalid mutually inductive types: `Optional` has 1 parameter(s), but the preceding type `Both` has 2

Note: All inductive types declared in the same `mutual` block must have the same parametersinductive Optional (α : Type u) where
    | none
    | some : α → Optional α
end

Invalid mutually inductive types: `Optional` has 1 parameter(s), but the preceding type `Both` has 2

Note: All inductive types declared in the same `mutual` block must have the same parameters

参数类型不一致

即使 Many 和 Optional 并非互递归，只要在同一个 mutual 块中声明，它们也必须具有完全相同的参数。两者都只有一个参数，但 Many 的参数未必与 Optional 的参数处于同一宇宙：

mutual
  inductive Many (α : Type) : Type u where
    | nil : Many α
    | cons : α → Many α → Many α
  Invalid mutually inductive types: Parameter `α` has type
  Type u
of sort `Type (u + 1)` but is expected to have type
  Type
of sort `Type 1`inductive Optional (α : Type u) where
    | none
    | some : α → Optional α
end

Invalid mutually inductive types: Parameter `α` has type
  Type u
of sort `Type (u + 1)` but is expected to have type
  Type
of sort `Type 1`

4.4.5.1.3. 宇宙层级🔗

互递归组中每个归纳类型的宇宙层级，同样需满足非互递归归纳类型的宇宙要求。另外，所有 mutual 组的类型必须位于同一宇宙，这意味着它们的构造子的参数也要受宇宙层级统一的限制。

宇宙层级不一致

这些互递归类型可以表示列表的行程编码（run-length encoding）：

mutual
  inductive RLE : List α → Type where
  | nil : RLE []
  | run (x : α) (n : Nat) :
    n ≠ 0 → PrefixRunOf n x xs ys → RLE ys → RLE xs

  inductive PrefixRunOf : Nat → α → List α → List α → Type where
  | zero
    (noMore : ¬∃zs, xs = x :: zs := by simp) :
    PrefixRunOf 0 x xs xs
  | succ :
    PrefixRunOf n x xs ys →
    PrefixRunOf (n + 1) x (x :: xs) ys
end

example : RLE [1, 1, 2, 2, 3, 1, 1, 1] :=
  .run 1 2 (by⊢ 2 ≠ 0 decideAll goals completed! 🐙) (.succ (.succ .zero)) <|
  .run 2 2 (by⊢ 2 ≠ 0 decideAll goals completed! 🐙) (.succ (.succ .zero)) <|
  .run 3 1 (by⊢ 1 ≠ 0 decideAll goals completed! 🐙) (.succ .zero) <|
  .run 1 3 (by⊢ 3 ≠ 0 decideAll goals completed! 🐙) (.succ (.succ (.succ (.zero)))) <|
  .nil

若将 PrefixRunOf 声明为 Prop 会更有意义，但类型因此不在同一宇宙，导致无法通过类型检查：

mutual
  inductive RLE : List α → Type where
  | nil : RLE []
  | run
    (x : α) (n : Nat) :
    n ≠ 0 → PrefixRunOf n x xs ys → RLE ys →
    RLE xs

  Invalid mutually inductive types: The resulting type of this declaration
  Prop
differs from a preceding one
  Type

Note: All inductive types declared in the same `mutual` block must belong to the same type universeinductive PrefixRunOf : Nat → α → List α → List α → Prop where
  | zero
    (noMore : ¬∃zs, xs = x :: zs := by simp) :
    PrefixRunOf 0 x xs xs
  | succ :
    PrefixRunOf n x xs ys →
    PrefixRunOf (n + 1) x (x :: xs) ys
end

Invalid mutually inductive types: The resulting type of this declaration
  Prop
differs from a preceding one
  Type

Note: All inductive types declared in the same `mutual` block must belong to the same type universe

这里也可以将性质单独定义，再通过子类型表达：

def RunLengths α := List (α × Nat)
def NoRepeats : RunLengths α → Prop
  | [] => True
  | [_] => True
  | (x, _) :: ((y, n) :: xs) =>
    x ≠ y ∧ NoRepeats ((y, n) :: xs)
def RunsMatch : RunLengths α → List α → Prop
  | [], [] => True
  | (x, n) :: xs, ys =>
    ys.take n = List.replicate n x ∧
    RunsMatch xs (ys.drop n)
  | _, _ => False
def NonZero : RunLengths α → Prop
  | [] => True
  | (_, n) :: xs => n ≠ 0 ∧ NonZero xs
structure RLE (xs : List α) where
  rle : RunLengths α
  noRepeats : NoRepeats rle
  runsMatch : RunsMatch rle xs
  nonZero : NonZero rle

example : RLE [1, 1, 2, 2, 3, 1, 1, 1] where
  rle := [(1, 2), (2, 2), (3, 1), (1, 3)]
  noRepeats := by⊢ NoRepeats [(1, 2), (2, 2), (3, 1), (1, 3)] simp [NoRepeats]All goals completed! 🐙
  runsMatch := by⊢ RunsMatch [(1, 2), (2, 2), (3, 1), (1, 3)] [1, 1, 2, 2, 3, 1, 1, 1] simp [RunsMatch]All goals completed! 🐙
  nonZero := by⊢ NonZero [(1, 2), (2, 2), (3, 1), (1, 3)] simp [NonZero]All goals completed! 🐙

4.4.5.1.4. 正性条件(Positivity)🔗

mutual 组中定义的每个归纳类型，只能严格正地出现在组内所有类型的所有构造子参数类型中。换言之，在组内每个构造子的每个参数类型中，组内类型构造子都不能出现在任何箭头左侧，也不能出现在参数位置，除非它是某个归纳类型的类型构造子的参数。

互递归条件下的严格正性

在下面的 mutual 组中，Tm 在 Binding.scope 的参数类型里出现在负位置：

mutual
  (kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declaredinductive Tm where
    | app : Tm → Tm → Tm
    | lam : Binding → Tm
  inductive Binding where
    | scope : (Tm → Tm) → Binding
end

由于 Tm 属于同一个互递归组，故只能严格正性出现。实际却出现在负位置：

(kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declared

嵌套位置

LocatedStx 和 Stx 这组互递归类型，递归出现均不在箭头左侧，且作为归纳类型类型构造子的参数，有严格正性：

mutual
  inductive LocatedStx where
    | mk (line col : Nat) (val : Stx)
  inductive Stx where
    | atom (str : String)
    | node (kind : String) (args : List LocatedStx)
end

在线查看 ↪

4.4.5.2. 递归子🔗

互递归归纳类型和非互递归归纳类型一样，都提供了原语递归子。这些递归子会考虑到需要处理组内的其他类型，因此每个归纳类型都会有一个目标参数。由于在 mutual 组中的所有归纳类型都被要求有相同的参数，递归子依然会首先接收这些参数，并将它们抽象到目标参数和递归子的其余部分上。此外，因为递归子必须处理组内的其他类型，所以它还需要为组内每个类型的每个构造子提供分支。实际上，类型之间具体的依赖关系在这里没有被考虑；即使由于互递归依赖关系较少，某些目标参数或构造子分支实际上并非必须，生成的递归子依旧会要求这些内容。

偶数与奇数

mutual
  inductive Even : Nat → Prop where
    | zero : Even 0
    | succ : Odd n → Even (n + 1)
  inductive Odd : Nat → Prop where
    | succ : Even n → Odd (n + 1)
end

Even.rec
  {motive_1 : (a : Nat) → Even a → Prop}
  {motive_2 : (a : Nat) → Odd a → Prop}
  (zero : motive_1 0 Even.zero)
  (succ : {n : Nat} → (a : Odd n) → motive_2 n a → motive_1 (n + 1) (Even.succ a)) :
  (∀ {n : Nat} (a : Even n), motive_1 n a → motive_2 (n + 1) (Odd.succ a)) →
  ∀ {a : Nat} (t : Even a), motive_1 a t

Odd.rec
  {motive_1 : (a : Nat) → Even a → Prop}
  {motive_2 : (a : Nat) → Odd a → Prop}
  (zero : motive_1 0 Even.zero)
  (succ : ∀ {n : Nat} (a : Odd n), motive_2 n a → motive_1 (n + 1) (Even.succ a)) :
  (∀ {n : Nat} (a : Even n), motive_1 n a → motive_2 (n + 1) (Odd.succ a)) → ∀ {a : Nat} (t : Odd a), motive_2 a t

在线查看 ↪

表面互递归类型

类型 Two 和 Three 其实互不引用，却作为一个 mutual 组共同声明：

mutual
  inductive Two (α : Type) where
    | mk : α → α → Two α
  inductive Three (α : Type) where
    | mk : α → α → α → Three α
end

Two 的递归子 Two.rec 依然需要 motive 以及 Three 的分支：

Two.rec.{u} {α : Type}
  {motive_1 : Two α → Sort u}
  {motive_2 : Three α → Sort u}
  (mk : (a a_1 : α) → motive_1 (Two.mk a a_1)) :
  ((a a_1 a_2 : α) → motive_2 (Three.mk a a_1 a_2)) → (t : Two α) → motive_1 t

在线查看 ↪

4.4.5.3. 运行时表示🔗

互递归归纳类型在编译后及运行期的表示，与非互递归归纳类型完全一致。对于互递归归纳类型的限制，是为了保证 Lean 作为一种逻辑的可靠性，不影响实际代码的编译与运行。

4.4.5.4. 嵌套归纳类型🔗

嵌套归纳类型是指这些归纳类型在定义中出现了递归自身类型，并且这些递归出现作为其他归纳类型构造子的参数。这些递归出现是“嵌套”在其他类型构造子之下的。只要满足一定条件，嵌套归纳类型就可以转换为互递归归纳类型；这种转换说明它们是可靠的。在内部，内核会执行这种转换；如果转换成功，那么原有的嵌套归纳类型会被接受。这样可以避免直接暴露内部转换细节而产生的性能和易用性问题。

嵌套递归出现必须满足以下要求：

它们必须直接嵌套在某个归纳类型的类型构造子之下。对于通过规约才变成嵌套出现的情况是不被接受的。
像构造子的参数这样的本地变量，不允许出现在嵌套递归出现的参数中。
嵌套递归出现必须处于严格正向位置。

嵌套归纳类型

自然数除了用两个构造子定义，也可以通过 Option 来定义：

inductive ONat : Type where
  | mk (pred : Option ONat)

可以有任意分支数的树，也叫 rose trees，它就是一种嵌套归纳类型：

inductive RTree (α : Type u) : Type u where
  | empty
  | node (val : α) (children : List (RTree α))

在线查看 ↪

非法的嵌套归纳类型

这个任意分支的蔷薇树声明使用了 List 的别名，而不是直接使用 List：

abbrev Children := List

(kernel) arg #3 of 'RTree.node' contains a non valid occurrence of the datatypes being declaredinductive RTree (α : Type u) : Type u where
  | empty
  | node (val : α) (children : Children (RTree α))

(kernel) arg #3 of 'RTree.node' contains a non valid occurrence of the datatypes being declared

这种定义方式用于通过一个索引追踪树的深度。构造子 DRTree.node 有一个自动隐式参数 n，代表所有子树的深度。然而，像构造子参数这样本地变量，不允许作为嵌套递归出现的参数：

(kernel) invalid nested inductive datatype 'List', nested inductive datatypes parameters cannot contain local variables.inductive DRTree (α : Type u) : Nat → Type u where
  | empty : DRTree α 0
  | node (val : α) (children : List (DRTree α n)) : DRTree α (n + 1)

下面的声明包含一个嵌套在 Option 下、并非严格正向的归纳类型出现：

(kernel) arg #1 of 'WithCheck.check' has a non positive occurrence of the datatypes being declaredinductive WithCheck where
  | done
  | check (f : Option WithCheck → Bool)

(kernel) arg #1 of 'WithCheck.check' has a non positive occurrence of the datatypes being declared

This rose tree has a branching factor that's limited by its parameter:

(kernel) application type mismatch
  List.length children
argument has type
  @_nested.List_1 branches α
but function has type
  List (@BRTree branches α) → Natinductive BRTree (branches : Nat) (α : Type u) : Type u where
  | mk :
    (children : List (BRTree branches α)) →
    children.length < branches →
    BRTree branches α

Only nested inductive types that can be translated to mutual inductive types are allowed. However, translating this type would require a translation of List.length to the translated types, but function definitions may not occur in mutual blocks with inductive types. The resulting error message shows that the function was not translated, but was applied to a term of the translated type:

(kernel) application type mismatch
  List.length children
argument has type
  @_nested.List_1 branches α
but function has type
  List (@BRTree branches α) → Nat

It is acceptable to use the parameter with the nested occurrence with fully polymorphic functions, such as id:

inductive Variable name `RTree''` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _RTree''

Note: This linter can be disabled with `set_option linter.unusedVariables false`RTree'' (α : Type u) : Type u where
  | mk :
    (children : List (BRTree branches α)) →
    id children = children →
    BRTree branches α

In this case, the function applies equally well to the translated version as it does to the original.

嵌套归纳类型转换为互递归归纳类型的过程如下：

嵌套出现变为新的归纳类型: 对嵌套出现的归纳类型会翻译为同一互递归组里的新归纳类型，替换原先的嵌套出现。这些新归纳类型拥有与外层归纳类型一样的构造子，只是在原参数位置用刚刚翻译后的新类型替代。原始归纳类型本身定义为重写后类型的别名。如果新类型依然是嵌套归纳类型（比如在 Array 下嵌套，因其构造子要用 List，就需要再次翻译到 List），则重复此流程。
构造嵌套类型之间的转换: 在外层归纳类型和新别名，及辅助类型之间，分别自动生成互相转换的函数，这些转换将被证明为互逆关系。
构造子重建: 原始类型的每个构造子定义为一个函数，返回翻译后类型的相应构造子，调用时会自动应用必要的转换。
递归子重建: 嵌套归纳类型的递归子则是结合翻译后类型的递归子而实现的。在这一步，嵌套出现的目标会先套上转换函数，而次要前提会以它们作为参数。构造子之间的互逆性证明是必要的，因为封装后的构造子是单方向转换，但在组合递归结构时需要转换后的结果。

翻译嵌套归纳类型

下面这个嵌套归纳类型表示自然数：

inductive ONat where
  | mk (pred : Option ONat) : ONat

ONat.rec.{u} {motive_1 : ONat → Sort u} {motive_2 : Option ONat → Sort u}
  (mk : (pred : Option ONat) → motive_2 pred → motive_1 (ONat.mk pred)) (none : motive_2 none)
  (some : (val : ONat) → motive_1 val → motive_2 (some val)) (t : ONat) : motive_1 t#check ONat.rec

内部翻译的第一步，是用辅助归纳类型“内联”嵌套出现的位置。这里嵌套发生在 Option 之下，所以辅助类型拥有 Option 的构造子，但其类型参数用 ONat' 替代：

mutual
inductive ONat' where
  | mk (pred : OptONat) : ONat'

inductive OptONat where
  | none
  | some : ONat' → OptONat
end

ONat' 就是 ONat 经过编码后的版本：

def ONat := ONat'

下一步是定义转换函数，用于在原始嵌套类型和辅助类型之间相互转换：

def OptONat.ofOption : Option ONat → OptONat
  | Option.none => OptONat.none
  | Option.some o => OptONat.some o
def OptONat.toOption : OptONat → Option ONat
  | OptONat.none => Option.none
  | OptONat.some o => Option.some o

这些相互转换的函数是互逆的：

Definition `OptONat.to_of_eq_id` is a proposition; use `theorem` instead of `def`

Note: This linter can be disabled with `set_option linter.defProp false`def OptONat.to_of_eq_id o :
    OptONat.toOption (ofOption o) = o := byo:Option ONat⊢ (ofOption o).toOption = o
  cases onone⊢ (ofOption Option.none).toOption = Option.nonesomeval✝:ONat⊢ (ofOption (Option.some val✝)).toOption = Option.some val✝ <;>none⊢ (ofOption Option.none).toOption = Option.nonesomeval✝:ONat⊢ (ofOption (Option.some val✝)).toOption = Option.some val✝ rflAll goals completed! 🐙
Definition `OptONat.of_to_eq_id` is a proposition; use `theorem` instead of `def`

Note: This linter can be disabled with `set_option linter.defProp false`def OptONat.of_to_eq_id o :
    OptONat.ofOption (OptONat.toOption o) = o := byo:OptONat⊢ ofOption o.toOption = o
  cases onone⊢ ofOption none.toOption = nonesomea✝:ONat'⊢ ofOption (some a✝).toOption = some a✝ <;>none⊢ ofOption none.toOption = nonesomea✝:ONat'⊢ ofOption (some a✝).toOption = some a✝ rflAll goals completed! 🐙

原始的构造子被翻译成对翻译后类型的构造子的调用，同时会对嵌套递归部分做适当类型转换：

def ONat.mk (pred : Option ONat) : ONat :=
  ONat'.mk (.ofOption pred)

最后，原类型的递归子也可以翻译。翻译后的递归子会通过翻译后类型的递归子来实现。原本嵌套递归位置会采用相应的转换函数，并且互逆性的证明可以在需要时重写类型：

noncomputable def ONat.rec
    {motive1 : ONat → Sort u}
    {motive2 : Option ONat → Sort u}
    (h1 :
      (pred : Option ONat) → motive2 pred →
      motive1 (ONat.mk pred))
    (h2 : motive2 none)
    (h3 : (o : ONat) → motive1 o → motive2 (some o)) :
    (t : ONat) → motive1 t :=
  @ONat'.rec motive1 (motive2 ∘ OptONat.toOption)
    (fun pred ih =>
      OptONat.of_to_eq_id pred ▸ h1 pred.toOption ih)
    h2
    h3

在线查看 ↪

4.4.5.5. Lattice-Theoretic Inductive and Coinductive Predicates🔗

The syntax of inductive type declarations can be used to specify both inductive and coinductive predicates. These are not a built-in feature of Lean's type system, but are instead elaborated to a suitable encoding. They are described in a dedicated section.